Corelab Seminar
2019-2020
Antonis Achilleos
A guide to monitorability
Abstract.
I will present recent work on runtime monitorability. Runtime
Verification (RV) is the technique of using a monitor to detect the
violation or satisfaction of a property at runtime. One question that we
ask is what properties we can monitor for. But even before giving an
answer, we must first understand what that question means. Although many
monitorability definitions exist, few are defined explicitly in terms of
the operational guarantees provided by monitors, ie, the computational
entities carrying out the verification. We view monitorability as a
spectrum, where the fewer guarantees that are required of monitors, the
more properties become monitorable. Accordingly, we present a
monitorability hierarchy based on this trade-off.
For regular, linear-time specifications, we give syntactic
characterisations of the hierarchy in Hennessy-Milner logic with
recursion. We then compare the obtained fragments with previous results
for the branching-time setting.
This is joint work with Luca Aceto, Adrian Francalanza, Anna
Ingólfsdóttir, and Karoliina Lehtinen.